$\forall$$A$:Type, $B$, $C$, $D$:($A$$\rightarrow$Type), $f$:$a$:$A$ fp$\rightarrow$ $B$($a$), $g$:$a$:$A$ fp$\rightarrow$ $C$($a$), ${\it eq}$:EqDecider($A$).
\\[0ex]($\forall$$a$:$A$. $a$ $\in$ dom($f$) $\Rightarrow$ $B$($a$) $\subseteq\rho$ $D$($a$))
\\[0ex]$\Rightarrow$ ($\forall$$a$:$A$. $a$ $\in$ dom($g$) $\Rightarrow$ $C$($a$) $\subseteq\rho$ $D$($a$))
\\[0ex]$\Rightarrow$ $f$ $\oplus$ $g$ $\in$ $a$:$A$ fp$\rightarrow$ $D$($a$)